finite-type() 

latex

Definitions	, (x  l), P  Q, t  T, x:A. B(x), prop{i:l}, P  Q, P  Q, P  Q, P  Q, b, A, b, Unit, x:A. B(x), ff, tt, guard(T)
Lemmas	finite-type-iff-list, eqtt to assert, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, iff transitivity, or functionality wrt iff, cons member, l member wf, btrue wf, bool wf, bfalse wf